Nuprl Lemma : ma-single-pre-true_wf 0,22
a:Id. precondition a: True  MsgA 
latex

DefinitionsMsgA, precondition a: True, mk-ma, x : v, Prop, True, State(ds), Top, , x:A. B(x), x. t(x), Id, IdLnk, t  T, Knd
Lemmasfpf-empty wf, top wf, IdLnk wf, ma-state wf, true wf, fpf-single wf, Knd wf, Id wf, mk-ma wf

origin